$\forall$$l$:IdLnk, ${\it da}$:fpf(Knd; $k$.Type), ${\it tg}$:Id.
\\[0ex]($\uparrow$fpf{-}dom(id{-}deq; ${\it tg}$; es{-}dt($l$; ${\it da}$))) $\Leftarrow\!\Rightarrow$ ($\uparrow$fpf{-}dom(Kind{-}deq; rcv($l$,${\it tg}$); ${\it da}$))